Nuprl Lemma : st-atoms-distinct_wf
0,22
postcript
pdf
T
:(Id
Type),
tab
:secret-table(
T
). atoms-distinct(
tab
)
Prop
latex
Definitions
Type
,
t
T
,
Id
,
x
:
A
B
(
x
)
,
x
:
A
.
B
(
x
)
,
secret-table(
T
)
,
{
x
:
A
|
B
(
x
) }
,
{
i
..
j
}
,
,
s
=
t
,
Prop
,
st-atom(
tab
;
n
)
,
Atom$n
,
P
Q
,
,
||
tab
||
,
#$n
,
atoms-distinct(
tab
)
Lemmas
int
seg
wf
,
st-length
wf
,
nat
wf
,
st-atom
wf
,
secret-table
wf
,
Id
wf
origin
T:(Id
Type), tab:secret-table(T). atoms-distinct(tab) 
Prop T:(IdType), tab:secret-table(T). atoms-distinct(tab) Prop TB(x)x:A. B(x)
}
Q